(ADDAXIOM EQ2
 ((FORALL X) ((FORALL Y) (IMPLIES (EQUAL X Y) (EQUAL Y X)))))

(ADDAXIOM EQ3
 ((FORALL X)
  ((FORALL Y)
   ((FORALL Z)
    (IMPLIES (AND (EQUAL X Y) (EQUAL Y Z)) (EQUAL X Z))))))

(ADDAXIOM TABLEEMPTY
 ((FORALL X)
  (IMPLIES (AND (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S0)))
	   (NOT (AT X TABLE S0)))))

(ADDAXIOM DIFFOBJ
 (AND (NOT (EQUAL BOX1 BOX2))
      (NOT (EQUAL BOX1 TABLE))
      (NOT (EQUAL BOX1 DOOR))
      (NOT (EQUAL BOX1 OUTSIDE))
      (NOT (EQUAL BOX2 TABLE))
      (NOT (EQUAL BOX2 DOOR))
      (NOT (EQUAL BOX2 OUTSIDE))
      (NOT (EQUAL TABLE DOOR))
      (NOT (EQUAL TABLE OUTSIDE))
      (NOT (EQUAL DOOR OUTSIDE))))

(ADDAXIOM ATONE
 ((FORALL X)
  ((FORALL P1)
   ((FORALL P2)
    ((FORALL S)
     (IMPLIES (AND (AT X P1 S) (AT X P2 S)) (EQUAL P1 P2)))))))

(ADDAXIOM REDDOOR
 ((THEREEXISTS X)
  (AND (RED X)
       (NOT (EQUAL X ROBOT))
       (AT X DOOR S0)
       ((FORALL Y)
	(IMPLIES
	 (AND (AT Y DOOR S0)
	      (NOT (EQUAL Y ROBOT))
	      (NOT (HOLDING Y S0)))
	 (RED Y))))))

(ADDAXIOM ISKEYBOX (OR (EQUAL KEYBOX BOX1) (EQUAL KEYBOX BOX2)))

(ADDAXIOM KEYBOX1
 ((THEREEXISTS X)
  (AND (KEY X)
       (NOT (EQUAL X ROBOT))
       (AT X KEYBOX S0)
       (NOT (HOLDING X S0)))))

(ADDAXIOM KEYBOX2
 ((FORALL Y)
  (IMPLIES
   (AND (AT Y KEYBOX S0) (NOT (EQUAL Y ROBOT)) (NOT (HOLDING Y S0)))
   (KEY Y))))

(ADDAXIOM B1B2 (NOT (EQUAL BOX1 BOX2)))

(ADDAXIOM B1T (NOT (EQUAL BOX1 TABLE)))

(ADDAXIOM B1D (NOT (EQUAL BOX1 DOOR)))

(ADDAXIOM B1O (NOT (EQUAL BOX1 OUTSIDE)))

(ADDAXIOM B2T (NOT (EQUAL BOX2 TABLE)))

(ADDAXIOM B2D (NOT (EQUAL BOX2 DOOR)))

(ADDAXIOM B2O (NOT (EQUAL BOX2 OUTSIDE)))

(ADDAXIOM TD (NOT (EQUAL TABLE DOOR)))

(ADDAXIOM TO (NOT (EQUAL TABLE OUTSIDE)))

(ADDAXIOM DO (NOT (EQUAL DOOR OUTSIDE)))

(ADDAXIOM HOLDING
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y)
    (IMPLIES (AND (AT ROBOT Y S) (HOLDING X S)) (AT X Y S))))))

(ADDAXIOM HOLD2
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y)
    (IMPLIES (AND (HOLDING X S) (HOLDING Y S)) (EQUAL X Y))))))

(ADDAXIOM PICKUP
 ((FORALL S)
  ((AND ((LAMBDA SP)
	 ((FORALL X)
	  ((FORALL Y) (EQUIVALENT (AT X Y S) (AT X Y SP)))))
	((FORALL Z)
	 (IMPLIES
	  (AND (AT ROBOT Z S)
	       ((THEREEXISTS X)
		(AND (NOT (EQUAL X ROBOT)) (AT X Z S))))
	  ((THEREEXISTS X) (HOLDING X SP)))))
   (PICKUP S))))

(ADDAXIOM GO1
 ((FORALL S)
  ((FORALL Z)
   ((FORALL W) (EQUIVALENT (HOLDING W S)
			   (HOLDING W (GOO Z S)))))))

(ADDAXIOM GO2
 ((FORALL S)
  ((FORALL Z)
   (IMPLIES
    (OR (NOT (EQUAL Z OUTSIDE))
	((THEREEXISTS X) (AND (AT X DOOR S) (KEY X))))
    (AT ROBOT Z (GOO Z S))))))

(ADDAXIOM GO3
 ((FORALL S)
  ((FORALL Z)
   ((FORALL X)
    ((FORALL Y)
     (IMPLIES
      (AND (AT X Y S) (NOT (EQUAL X ROBOT)) (NOT (HOLDING X S)))
      (AT X Y (GOO Z S))))))))

(ADDAXIOM GO4
 (IMPLIES
  (AND ((FORALL S)
	((FORALL Y) ((FORALL X) (NOT (AND (AT X DOOR S) (KEY X))))))
       (AT ROBOT Y S))
  (AT ROBOT Y (GOO OUTSIDE S))))

(ADDAXIOM GO5
 ((FORALL S)
  ((FORALL Z)
   ((FORALL X)
    ((FORALL Y)
     (IMPLIES
      (AND (NOT (EQUAL X ROBOT))
	   (NOT (HOLDING X S))
	   (AT X Y (GOO Z S)))
      (AT X Y S)))))))

(ADDAXIOM RELEASE1
 ((FORALL S)
  ((FORALL X)
   ((FORALL Y) (EQUIVALENT (AT X Y S) (AT X Y (RELEASE S)))))))

(ADDAXIOM RELEASE2
 ((FORALL S) ((FORALL X) (NOT (HOLDING X (RELEASE S))))))

(GIVEPROOF TRY
 ((1 (NEQ PFROM OUTSIDE) (ASS (NEQ PFROM OUTSIDE)) (1))
  (2 (NEQ PTO OUTSIDE) (ASS (NEQ PTO OUTSIDE)) (2))
  (3 (AND ((FORALL X)
	   ((FORALL Y)
	    (EQUIVALENT (AT X Y SIT) (AT X Y (PICKUP SIT)))))
	  ((FORALL Z)
	   (IMPLIES
	    (AND (AT ROBOT Z SIT)
		 ((THEREEXISTS X) (AND (NEQ X ROBOT) (AT X Z SIT))))
	    ((THEREEXISTS X) (HOLDING X (PICKUP SIT))))))
     (ASS (AND ((FORALL X)
		((FORALL Y)
		 (EQUIVALENT (AT X Y SIT) (AT X Y (PICKUP SIT)))))
	       ((FORALL Z)
		(IMPLIES
		 (AND (AT ROBOT Z SIT)
		      ((THEREEXISTS X)
		       (AND (NEQ X ROBOT) (AT X Z SIT))))
		 ((THEREEXISTS X) (HOLDING X (PICKUP SIT)))))))
     (3))
  (4 (IMPLIES
      (OR (NOT (EQUAL PFROM OUTSIDE))
	  ((THEREEXISTS X) (AND (AT X DOOR S) (KEY X))))
      (AT ROBOT PFROM (GOO PFROM S)))
     (USEAX GO2 S PFROM)
     NIL)
  (5 (NOT (EQUAL PFROM OUTSIDE))
     (ASS (NOT (EQUAL PFROM OUTSIDE)))
     (5))
  (6 (AT ROBOT PFROM (GOO PFROM S))
     (TAUT (AT ROBOT PFROM (GOO PFROM S)) 4 5)
     (5))
  (7 (SETQ SIT (GOO PFROM S)) (DEF SIT (GOO PFROM S)) (7))
  (8 (AND ((FORALL X)
	   ((FORALL Y)
	    (EQUIVALENT (AT X Y (GOO PFROM S))
			(AT X Y (PICKUP (GOO PFROM S))))))
	  ((FORALL Z)
	   (IMPLIES
	    (AND (AT ROBOT Z (GOO PFROM S))
		 ((THEREEXISTS X)
		  (AND (NEQ X ROBOT) (AT X Z (GOO PFROM S)))))
	    ((THEREEXISTS X) (HOLDING X
				      (PICKUP (GOO PFROM
						   S)))))))
     (REP 3 7 1)
     (3 7))
  (9 ((FORALL Z)
      (IMPLIES
       (AND (AT ROBOT Z (GOO PFROM S))
	    ((THEREEXISTS X)
	     (AND (NEQ X ROBOT) (AT X Z (GOO PFROM S)))))
       ((THEREEXISTS X) (HOLDING X (PICKUP (GOO PFROM S))))))
     (AE 8 2)
     (3 7))
  (10 (IMPLIES
       (AND (AT ROBOT PFROM (GOO PFROM S))
	    ((THEREEXISTS X)
	     (AND (NEQ X ROBOT) (AT X PFROM (GOO PFROM S)))))
       ((THEREEXISTS X) (HOLDING X (PICKUP (GOO PFROM S)))))
      (US 9 PFROM)
      (3 7))
  (11 (AT OBJECT PFROM S) (ASS (AT OBJECT PFROM S)) (11))
  (12 (NEQ OBJECT ROBOT) (ASS (NEQ OBJECT ROBOT)) (12))
  (13 (HOLDING OBJECT S) (ASS (HOLDING OBJECT S)) (13))
  (14 (IMPLIES
       (AND (AT ROBOT PFROM (GOO PFROM S))
	    (HOLDING OBJECT (GOO PFROM S)))
       (AT OBJECT PFROM (GOO PFROM S)))
      (USEAX HOLDING (GOO PFROM S) OBJECT PFROM)
      NIL)
  (15 (EQUIVALENT (HOLDING OBJECT S) (HOLDING OBJECT (GOO PFROM S)))
      (USEAX GO1 S PFROM OBJECT)
      NIL)
  (16 (IMPLIES (HOLDING OBJECT S) (HOLDING OBJECT (GOO PFROM S)))
      (EQE 15 1)
      NIL)
  (17 (HOLDING OBJECT (GOO PFROM S)) (MP 13 16) (13))
  (18 (AND (AT ROBOT PFROM (GOO PFROM S))
	   (HOLDING OBJECT (GOO PFROM S)))
      (AI 6 17)
      (5 13))
  (19 (AT OBJECT PFROM (GOO PFROM S)) (MP 18 14) (13 5))
  (20 (NOT (HOLDING OBJECT S)) (ASS (NOT (HOLDING OBJECT S))) (20))
  (21 (IMPLIES
       (AND (AT OBJECT PFROM S)
	    (NOT (EQUAL OBJECT ROBOT))
	    (NOT (HOLDING OBJECT S)))
       (AT OBJECT PFROM (GOO PFROM S)))
      (USEAX GO3 S PFROM OBJECT PFROM)
      NIL)
  (22 (NOT (EQUAL OBJECT ROBOT))
      (ASS (NOT (EQUAL OBJECT ROBOT)))
      (22))
  (23 (AND (NOT (HOLDING OBJECT S))
	   (NOT (EQUAL OBJECT ROBOT))
	   (AT OBJECT PFROM S))
      (AI 20 22 11)
      (20 22 11))
  (24 (AND (AT OBJECT PFROM S)
	   (NOT (EQUAL OBJECT ROBOT))
	   (NOT (HOLDING OBJECT S)))
      (AI 11 22 20)
      (11 22 20))
  (25 (AT OBJECT PFROM (GOO PFROM S)) (MP 21 24) (11 22 20))
  (26 (IMPLIES (NOT (HOLDING OBJECT S))
	       (AT OBJECT PFROM (GOO PFROM S)))
      (DED 25 20)
      (11 22))
  (27 (IMPLIES (HOLDING OBJECT S) (AT OBJECT PFROM (GOO PFROM S)))
      (DED 19 13)
      (5))
  (28 (AT OBJECT PFROM (GOO PFROM S)) ((ALT 26 27)) (22 11 5))))